WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app,goal,naiverev,notEmpty} and constructors {Cons,False
,Nil,True}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
app#(Nil(),ys) -> c_2()
goal#(xs) -> c_3(naiverev#(xs))
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
naiverev#(Nil()) -> c_5()
notEmpty#(Cons(x,xs)) -> c_6()
notEmpty#(Nil()) -> c_7()
Weak DPs
and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
app#(Nil(),ys) -> c_2()
goal#(xs) -> c_3(naiverev#(xs))
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
naiverev#(Nil()) -> c_5()
notEmpty#(Cons(x,xs)) -> c_6()
notEmpty#(Nil()) -> c_7()
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,5,6,7}
by application of
Pre({2,5,6,7}) = {1,3,4}.
Here rules are labelled as follows:
1: app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
2: app#(Nil(),ys) -> c_2()
3: goal#(xs) -> c_3(naiverev#(xs))
4: naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
5: naiverev#(Nil()) -> c_5()
6: notEmpty#(Cons(x,xs)) -> c_6()
7: notEmpty#(Nil()) -> c_7()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
goal#(xs) -> c_3(naiverev#(xs))
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
- Weak DPs:
app#(Nil(),ys) -> c_2()
naiverev#(Nil()) -> c_5()
notEmpty#(Cons(x,xs)) -> c_6()
notEmpty#(Nil()) -> c_7()
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
-->_1 app#(Nil(),ys) -> c_2():4
-->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
2:S:goal#(xs) -> c_3(naiverev#(xs))
-->_1 naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs)):3
-->_1 naiverev#(Nil()) -> c_5():5
3:S:naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
-->_2 naiverev#(Nil()) -> c_5():5
-->_1 app#(Nil(),ys) -> c_2():4
-->_2 naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs)):3
-->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
4:W:app#(Nil(),ys) -> c_2()
5:W:naiverev#(Nil()) -> c_5()
6:W:notEmpty#(Cons(x,xs)) -> c_6()
7:W:notEmpty#(Nil()) -> c_7()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: notEmpty#(Nil()) -> c_7()
6: notEmpty#(Cons(x,xs)) -> c_6()
5: naiverev#(Nil()) -> c_5()
4: app#(Nil(),ys) -> c_2()
* Step 4: RemoveHeads WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
goal#(xs) -> c_3(naiverev#(xs))
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
-->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
2:S:goal#(xs) -> c_3(naiverev#(xs))
-->_1 naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs)):3
3:S:naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
-->_2 naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs)):3
-->_1 app#(Cons(x,xs),ys) -> c_1(app#(xs,ys)):1
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(2,goal#(xs) -> c_3(naiverev#(xs)))]
* Step 5: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
goal(xs) -> naiverev(xs)
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
notEmpty(Cons(x,xs)) -> True()
notEmpty(Nil()) -> False()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
* Step 6: DecomposeDG WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
and a lower component
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
Further, following extension rules are added to the lower component.
naiverev#(Cons(x,xs)) -> app#(naiverev(xs),Cons(x,Nil()))
naiverev#(Cons(x,xs)) -> naiverev#(xs)
** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs))
-->_2 naiverev#(Cons(x,xs)) -> c_4(app#(naiverev(xs),Cons(x,Nil())),naiverev#(xs)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
naiverev#(Cons(x,xs)) -> c_4(naiverev#(xs))
** Step 6.a:2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
naiverev#(Cons(x,xs)) -> c_4(naiverev#(xs))
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
naiverev#(Cons(x,xs)) -> c_4(naiverev#(xs))
** Step 6.a:3: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
naiverev#(Cons(x,xs)) -> c_4(naiverev#(xs))
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Cons :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
naiverev# :: ["A"(1)] -(15)-> "A"(0)
c_4 :: ["A"(0)] -(0)-> "A"(14)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Cons_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
"c_4_A" :: ["A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
naiverev#(Cons(x,xs)) -> c_4(naiverev#(xs))
2. Weak:
** Step 6.b:1: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
- Weak DPs:
naiverev#(Cons(x,xs)) -> app#(naiverev(xs),Cons(x,Nil()))
naiverev#(Cons(x,xs)) -> naiverev#(xs)
- Weak TRS:
app(Cons(x,xs),ys) -> Cons(x,app(xs,ys))
app(Nil(),ys) -> ys
naiverev(Cons(x,xs)) -> app(naiverev(xs),Cons(x,Nil()))
naiverev(Nil()) -> Nil()
- Signature:
{app/2,goal/1,naiverev/1,notEmpty/1,app#/2,goal#/1,naiverev#/1,notEmpty#/1} / {Cons/2,False/0,Nil/0,True/0
,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/0,c_7/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {app#,goal#,naiverev#,notEmpty#} and constructors {Cons
,False,Nil,True}
+ Applied Processor:
Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
+ Details:
Signatures used:
----------------
Cons :: ["A"(2) x "A"(2)] -(2)-> "A"(2)
Cons :: ["A"(11) x "A"(11)] -(11)-> "A"(11)
Cons :: ["A"(15) x "A"(15)] -(15)-> "A"(15)
Cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
Nil :: [] -(0)-> "A"(2)
Nil :: [] -(0)-> "A"(11)
Nil :: [] -(0)-> "A"(6)
Nil :: [] -(0)-> "A"(15)
Nil :: [] -(0)-> "A"(12)
app :: ["A"(2) x "A"(2)] -(1)-> "A"(2)
naiverev :: ["A"(11)] -(1)-> "A"(2)
app# :: ["A"(2) x "A"(0)] -(3)-> "A"(0)
naiverev# :: ["A"(15)] -(0)-> "A"(0)
c_1 :: ["A"(0)] -(0)-> "A"(14)
Cost-free Signatures used:
--------------------------
Base Constructor Signatures used:
---------------------------------
"Cons_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
"Nil_A" :: [] -(0)-> "A"(1)
"c_1_A" :: ["A"(0)] -(0)-> "A"(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
app#(Cons(x,xs),ys) -> c_1(app#(xs,ys))
2. Weak:
WORST_CASE(?,O(n^2))